\begin{tabbing}
es{-}independent(${\it es}$; $i$; $k$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$s_{1}$:es\_state(${\it es}$; $i$), $s_{2}$:es\_state(${\it es}$; $i$).\+
\\[0ex]es{-}x{-}equiv(${\it es}$; $i$; $x$; $s_{1}$; $s_{2}$)
\\[0ex]$\Rightarrow$ \=(($\forall$$v$:es{-}kindtype(${\it es}$; $i$; $k$). \+
\\[0ex]es{-}x{-}equiv(${\it es}$; $i$; $x$; (es{-}trans(${\it es}$; $i$)($k$,$v$,$s_{1}$)); (es{-}trans(${\it es}$; $i$)($k$,$v$,$s_{2}$)))
\\[0ex]$\wedge$ (\=es{-}send(${\it es}$; $i$)($k$,$v$,es{-}read{-}state($s_{1}$))\+
\\[0ex]=
\\[0ex]es{-}send(${\it es}$; $i$)($k$,$v$,es{-}read{-}state($s_{2}$))
\\[0ex]$\in$ (es{-}Msg(${\it es}$) List)))
\-\\[0ex]$\wedge$ \=(($\uparrow$islocal($k$))\+
\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$. \+
\\[0ex]es{-}choose(${\it es}$; $i$)(act($k$),$n$,es{-}read{-}state($s_{1}$))
\\[0ex]=
\\[0ex]es{-}choose(${\it es}$; $i$)(act($k$),$n$,es{-}read{-}state($s_{2}$))
\\[0ex]$\in$ (es{-}kindtype(${\it es}$; $i$; $k$) + Unit))))
\-\-\-\-
\end{tabbing}